home *** CD-ROM | disk | FTP | other *** search
/ The PC-SIG Library 9 / The PC-SIG Library on CD ROM - Ninth Edition.iso / 401_500 / DISK0417 / DISK0417.ZIP / PROLOG.ARC / LOGIC.ARC / SKOLEM.PRO < prev   
Text File  |  1986-11-07  |  4KB  |  141 lines
  1. translate(X) :-
  2.    implout(X,X1),           /* Stage 1 */
  3.    negin(X1,X2),            /* Stage 2 */
  4.    skolemiz(X2,X3,[]),        /* Stage 3 */
  5.    univout(X3,X4),          /* Stage 4 */
  6.    conjn(X4,X5),            /* Stage 5 */
  7.    clausify(X5,Clauses,[]), /* Stage 6 */
  8.    pclauses(Clauses).       /* Print out clauses */
  9.  
  10. implout((P <-> Q),((P1 & Q1) # (~P1 & ~Q1))) :- !,
  11.    implout(P,P1), implout(Q,Q1).
  12. implout((P -> Q),(~P1 # Q1)) :- !,
  13.    implout(P,P1), implout(Q,Q1).
  14. implout(all(X,P),all(X,P1)) :- !,
  15.    implout(P,P1).
  16. implout(exists(X,P),exists(X,P1)) :- !,
  17.    implout(P,P1).
  18. implout((P & Q),(P1 & Q1)) :- !,
  19.    implout(P,P1), implout(Q,Q1).
  20. implout((P # Q),(P1 # Q1)) :- !,
  21.    implout(P,P1), implout(Q,Q1).
  22. implout((~P),(~P1)) :- !,
  23.    implout(P1).
  24. implout(P,P).
  25.  
  26. negin((~P),P1) :- !, neg(P,P1).
  27. negin(all(X,P),all(X,P1)) :- !, negin(P,P1).
  28. negin(exists(X,P),exists(X,P1)) :- !, negin(P,P1).
  29. negin((P & Q),(P1 & Q1)) :- !, negin(P,P1), negin(Q,Q1).
  30. negin((P # Q),(P1 # Q1)) :- !, negin(P,P1), negin(Q,Q1).
  31. negin(P,P).
  32.  
  33.    neg((~P),P1) :- !, negin(P,P1).
  34.    neg(all(X,P),exists(X,P1)) :- !, neg(P,P1).
  35.    neg(exists(X,P),all(X,P1)) :- !, neg(P,P1).
  36.    neg((P & Q),(P1 # Q1)) :- !, neg(P,P1), neg(Q,Q1).
  37.    neg((P # Q),(P1 & Q1)) :- !, neg(P,P1), neg(Q,Q1).
  38.    neg(P,(~P)).
  39.  
  40. skolemiz(all(X,P),all(X,P1),Vars) :- !, skolemiz(P,P1,[X|Vars]).
  41. skolemiz(exists(X,P),P2,Vars) :- !,
  42.    gensym(f,F),
  43.    Sk =.. [F|Vars],
  44.    P =.. [Ph|Pt],
  45.    subsk(X,Sk,Pt,P1t),
  46.    P1 =.. [Ph|P1t],
  47.    skolemiz(P1,P2,Vars).
  48. skolemiz((P # Q),(P1 # Q1),Vars) :- !,
  49.    skolemiz(P,P1,Vars), skolemiz(Q,Q1,Vars).
  50. skolemiz((P & Q),(P1 & Q1),Vars) :- !,
  51.    skolemiz(P,P1,Vars), skolemiz(Q,Q1,Vars).
  52. skolemiz(P,P,_).
  53.  
  54.    subsk(_,_,[],[]).
  55.    subsk(X,A,[Y|L],[A|M]) :- X==Y ,subsk(X,A,L,M).
  56.    subsk(X,A,[Y|L],[Y|M]) :- X\==Y ,subsk(X,A,L,M).
  57.  
  58. univout(all(X,P),P1) :- !, univout(P,P1).
  59. univout((P&Q),(P1&Q1)) :- !,
  60.    univout(P,P1), univout(Q,Q1).
  61. univout((P#Q),(P1#Q1)) :- !,
  62.    univout(P,P1), univout(Q,Q1).
  63. univout(P,P).
  64.  
  65. conjn((P#Q),R) :- !,
  66.    conjn(P,P1), conjn(Q,Q1), conjn1((P1#Q1),R).
  67. conjn((P&Q),(P1&Q1)) :- !,
  68.    conjn(P,P1), conjn(Q,Q1).
  69. conjn(P,P).
  70.  
  71.    conjn1(((P&Q)#R),(P1&Q1)) :- !,
  72.       conjn((P#R),P1), conjn((Q#R),Q1).
  73.    conjn1((P#(Q&R)),(P1&Q1)) :- !,
  74.       conjn((P#Q),P1), conjn((P#R),Q1).
  75.    conjn1(P,P).
  76.  
  77. clausify((P&Q),C1,C2) :- !,
  78.    clausify(P,C1,C3), clausify(Q,C3,C2).
  79. clausify(P,[cl(A,B)|Cs],Cs) :- inclause(P,A,[],B,[]), !.
  80. clausify(_,C,C).
  81.  
  82.    inclause((P#Q),A,A1,B,B1) :- !,
  83.       inclause(P,A2,A1,B2,B1), inclause(Q,A,A2,B,B2).
  84.    inclause((~P),A,A,B1,B) :- !,
  85.       notin(P,A), putin(P,B,B1).
  86.    inclause(P,A1,A,B,B) :- notin(P,B), putin(P,A,A1).
  87.  
  88.       notin(X,[X|_]) :- !, fail.
  89.       notin(X,[_|L]) :- !, notin(X,L).
  90.       notin(X,[]).
  91.  
  92.       putin(X,[],[X]) :- !.
  93.       putin(X,[X|L],L) :- !.
  94.       putin(X,[Y|L],[Y|L1]) :- putin(X,L,L1).
  95.  
  96. pclauses([]) :- !, nl, nl.
  97. pclauses([cl(A,B)|Cs]) :- pclause(A,B), nl, pclauses(Cs).
  98.  
  99.    pclause(L,[]) :- !, pdisj(L), print('.').
  100.    pclause([],L) :- !, print(':- '), pconj(L), print('.').
  101.    pclause(L1,L2) :- pdisj(L1), print(' :- '), pconj(L2),
  102.       print('.').
  103.  
  104.       pdisj([L]) :- !, print(L).
  105.       pdisj([L|Ls]) :- print(L), print('; '), pdisj(Ls).
  106.  
  107.       pconj([L]) :- !, print(L).
  108.       pconj([L|Ls]) :- print(L), print(', '), pconj(Ls).
  109.  
  110.  
  111. /* Create a new atom starting with a root provided
  112.    and finishing with a unique number              */
  113.  
  114. gensym(Root,Atom) :-
  115.    get_num(Root,Num),
  116.    name(Root,Name1),
  117.    integer_name(Num,Name2),
  118.    append(Name1,Name2,Name),
  119.    name(Atom,Name).
  120.  
  121. get_num(Root,Num) :-     /* This root encountered before */
  122.    retract(current_num(Root,Num1)), !,
  123.    Num is Num1 + 1,
  124.    asserta(current_num(Root,Num)).
  125. get_num(Root,1) :-       /* First time for this root */
  126.    asserta(current_num(Root,1)).
  127.  
  128. /* Convert from an integer to a list of characters */
  129.  
  130. integer_name(Int,List) :- integer_name(Int,[],List).
  131.  
  132. integer_name(I,SoFar,[C|SoFar]) :- I < 10, !, C is I + 48.
  133. integer_name(I,SoFar,List) :-
  134.    TopHalf is I / 10,
  135.    BotHalf is I mod 10,
  136.    C is BotHalf + 48,
  137.    integer_name(TopHalf,[C|SoFar],List).
  138.  
  139. append([],L,L).
  140. append([X|L1],L2,[X|L3]) :- append(L1,L2,L3).
  141.